r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s)) 

latex

Definitions	Prop, CoPrime(a,b), x:A. B(x), t  T, , SqStable(P), P  Q, T, True, x:A. B(x), P & Q, a = b mod m, P  Q, x:A. B(x), b | a
Lemmas	divides reflexivity, divisor of mul, divisor of minus, divides wf, true wf, squash wf, eqmod wf, coprime bezout id, sq stable coprime, nat plus wf, coprime wf